Condensed detachment

Condensed detachment (Rule D) is a method of finding the most general possible conclusion given two formal logical statements. It was developed by the Irish logician Carew Meredith in the 1950s and inspired by the work of Łukasiewicz.

Contents 1 Informal description 2 D-notation 3 Advantages 4 References

Informal description

A rule of detachment says:
"Given that implies , and given , infer ."

The condensed detachment goes a step further and says:
"Given that implies , and given an , use a unifier of and to make and of the same form, then use a standard rule of detachment."

A substitution A that when applied to produces , and substitution B that when applied to produces , are called the Unifiers of and .

Various unifiers may produce expressions with varying numbers of free variables. Some possible unifying expressions are substitution instances of others. If one expression is a substitution instance of another (and not just a variable renaming), then that other is called "more general".

If the most general unifier is used in condensed detachment, then the logical result is the most general conclusion that can be made in the given inference with the given second expression. (And since any weaker inference you can get is a substitution instance of the most general one, nothing less than the most general unifier is ever used in practice.)

In some logics (such as standard PC) have a set of defining axioms with the "D-completeness" property. If a set of axioms is D-Complete, then any vaild theorems of the system can be generated by condensed detachment alone. Note that "D-completeness" is a property of an axiomatic basis for a system, not an intrinsic property of a logic system itself.

J.A.Kalman proved that any conclusion that can be generated by a sequence of uniform substitution and modus ponens steps can either be generated by condensed detachment alone, or is a substitution instance of something that can be generated by condensed detachment alone. This makes condensed detachment useful for any logic system that has modus ponens and substitution, regardless of whether or not it is D-complete.

D-notation

Since a given major premise and a given minor premise uniquely determine the conclusion (up to variable renaming), Meredith observed that it was only necessary to note which two statements were involved and that the condensed detachment can be used without any other notation required. This led to the "D-notation" for proofs. This notation uses the "D" operator to mean condensed detachment, and takes 2 arguments, in a standard prefix notation string. For example, if you have four axioms a typical proof in D-notation might look like: DD12D34 which shows a condensed detachment step using the result of two prior condensed detachment steps, the first of which used axioms 1 and 2, and the second of which used axioms 3 and 4.

This notation, besides being used in some automated theorem provers, sometimes appears in catalogs of proofs

Condensed detachment's use of unification predates the resolution techniques of automated theorem proving.

Advantages

For automated theorem proving condensed detachment has a number of advantages over raw modus ponens and uniform substitution.

At a Modus Ponens and substitution proof you have an infinite number of choices for what you can substitute for variables. This means that you have an infinite number of possible next steps. With condensed detachment there are only a finite number of possible next steps in a proof.

The D-notation for complete condensed detachment proofs allows easy description of proofs for cataloging and search. A typical complete 30 step proof is less than 60 characters long in D-notation (excluding the statement of the axioms.)

References

• Condensed Detachment as a Rule of inference, J.A.Kalman, Studia Logica, Volume 42, Number 4, December, 1983
• Hindley, J. Roger (1993), "BCK and BCI logics, condensed detachment and the $2$-property", Notre Dame Journal of Formal Logic 34 (2): 231–250, doi:10.1305/ndjfl/1093634655, MR1231287, http://projecteuclid.org/Dienst/UI/1.0/Summarize/euclid.ndjfl/1093634655 
• Experiments in Automated Deduction with Condensed Detachment, William McCune and Larry Wos, Proceedings of the 11th International Conference on Automated Deduction (1992)

Logic   Overview Academic areas Argumentation theory Axiology Critical thinking Computability theory Formal semantics History of logic Informal logic Logic in computer science Mathematical logic Mathematics Metalogic Metamathematics Model theory Philosophical logic Philosophy Philosophy of logic Philosophy of mathematics Proof theory Set theory Foundational concepts Abduction Analytic truth Antinomy A priori Deduction Definition Description Entailment Induction Inference Logical consequence Logical form Logical implication Logical truth Name Necessity Meaning Paradox Possible world Presupposition Probability Reason Reasoning Reference Semantics Statement Strict implication Substitution Syntax Truth Truth value Validity   Philosophical logic Critical thinking and Informal logic Analysis Ambiguity Argument Belief Bias Credibility Evidence Explanation Explanatory power Fact Fallacy Inquiry Opinion Parsimony Premise Propaganda Prudence Reasoning Relevance Rhetoric Rigor Vagueness Theories of deduction Constructivism Dialetheism Fictionalism Finitism Formalism Intuitionism Logical atomism Logicism Nominalism Platonic realism Pragmatism Realism   Metalogic and metamathematics Cantor's theorem Church's theorem Church's thesis Consistency Effective method Foundations of mathematics Gödel's completeness theorem Gödel's incompleteness theorems Soundness Completeness Decidability Interpretation Löwenheim–Skolem theorem Metatheorem Satisfiability Independence Type–token distinction Use–mention distinction   Mathematical logic General Formal language Formation rule Formal system Deductive system Formal proof Formal semantics Well-formed formula Set Element Class Classical logic Axiom Natural deduction Rule of inference Relation Theorem Logical consequence Axiomatic system Type theory Symbol Syntax Theory Traditional logic Proposition Inference Argument Validity Cogency Syllogism Square of opposition Venn diagram Propositional calculus and Boolean logic Boolean functions Propositional calculus Propositional formula Logical connectives Truth tables Predicate First-order Quantifiers Predicate Second-order Monadic predicate calculus Set theory Set Empty set Enumeration Extensionality Finite set Function Subset Power set Countable set Recursive set Domain Range Ordered pair Uncountable set Model theory Model Interpretation Non-standard model Finite model theory Truth value Validity Proof theory Formal proof Deductive system Formal system Theorem Logical consequence Rule of inference Syntax Computability theory Recursion Recursive set Recursively enumerable set Decision problem Church–Turing thesis Computable function Primitive recursive function   Non-classical logic Modal logic Alethic Axiologic Deontic Doxastic Epistemic Temporal Intuitionism Intuitionistic logic Constructive analysis Heyting arithmetic Intuitionistic type theory Constructive set theory Fuzzy logic Degree of truth Fuzzy rule Fuzzy set Fuzzy finite element Fuzzy set operations Substructural logic Structural rule Relevance logic Linear logic Paraconsistent logic Dialetheism Description logic Ontology Ontology language   Logicians Anderson Aristotle Averroes Avicenna Bain Barwise Bernays Boole Boolos Cantor Carnap Church Chrysippus Curry De Morgan Frege Geach Gentzen Gödel Hilbert Kleene Kripke Leibniz Löwenheim Peano Peirce Putnam Quine Russell Schröder Scotus Skolem Smullyan Tarski Turing Whitehead William of Ockham Wittgenstein Zermelo   Lists Topics Outline of logic Index of logic articles Mathematical logic Boolean algebra Set theory Other Logicians Rules of inference Paradoxes Fallacies Logic symbols Portal Category Outline WikiProject Talk changes